Static analysis involves analyzing a program without actually dynamically testing the program through execution. For example, static analysis may determine if there are errors in the program without run-time testing the program. In other cases, static analysis can be combined with run-time testing. For example, a dynamic control system can use static analysis to direct run-time testing.
Typically, static analysis involves the symbolic evaluation of a set of predicates. Predicates represent relations between variables, properties, etc. The predicates may pertain in various ways to the program being analyzed. For example, some predicates can be extracted directly from the program, e.g., from conditional statements (e.g., “IF” statements) in the program. Other predicates can be computed using various types of transformations applied to program statements.
Static analysis may rely on a theorem prover to analyze the identified predicates. A theorem prover typically accepts input information expressed in a specified format, as determined by a background theory. The theorem prover performs logical analysis on the input information in the symbolic domain to produce a conclusion. For example, in one case, the theorem prover can determine whether there is a contradiction in a set of predicates; if so, this means that the conjunction of all predicates yields FALSE for any values for predicate variables. Some theorem provers analyze the input information with reference to constraints specified by axioms. Axioms may be regarded as domain-specific predicates a priori assumed as yielding TRUE. In general, predicate evaluation is a complex task, particularly when dealing with a large number of predicates or complex predicates. As a result, in designing a physical implementation of such analysis, it is appropriate to keep in mind temporal and memory limitations that may affect performance of the implementation.
A predicate that contains pointer information relates some term in the predicate to a memory location. To facilitate automatic analysis of such predicates, it is appropriate to convert such pointer information into a form that can be readily interpreted by a theorem prover. However, there is currently no fully adequate theory for expressing such pointer information. One known approach uses precise axioms that reflect a physical memory model of a programming language (e.g., by mapping any pointer-based computation to an array-based computation). While being precise, this method is computationally complex and may not easily scale for large program code. Another approach uses pointer axioms that attempt to approximate a logical memory model, with the core axiom being Dereference(Address(x))==x. This approach scales well, but it is not precise, e.g., because it does not take into account various scenarios, such as semantically incorrect pointer dereferences (which can result from programs that are incorrect). To address this shortcoming, the approach uses various work-around patches.
The lack of an adequate theory for pointers can have various negative consequences. For example, this deficiency can lead to analysis that includes unsound results, such as incorrect or incomplete results. Further, the deficiency can result in poor performance of a program analysis engine, e.g., by consuming too much memory and/or time. Further, the lack of an adequate theory can result in poor integration of predicate analysis functionality with other aspects of the program analysis engine, which, in turn, may also negatively impact accuracy and performance.